FDL - Step of Proof: mul_cancel_in

Step of Proof: mul_cancel_in_eq

12,41

Inference at *
Iof proof for Lemma mul cancel in eq:

a, b:

, n:

. ((n * a) = (n * b))

(a = b)

by ((RepeatMFor 3 (D 0))

CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat

C3:n)) (first_tok :t) inil_term)))

C1:

C1: 1. a :

C1: 2. b :

C1: 3. n :

C1:

((n * a) = (n * b))

(a = b)

Definitions t T, x:A. B(x)

Lemmas int nzero wf